0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 389 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 399 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 1 ms)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇒, 0 ms)
↳23 QDP
↳24 QDPSizeChangeProof (⇔, 0 ms)
↳25 YES
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, void), tree(s(X1), void, void)) → U9_GAG(X1, X2, pB_in_ga(X1, X2))
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, void), tree(s(X1), void, void)) → PB_IN_GA(X1, X2)
PB_IN_GA(X1, X2) → U2_GA(X1, X2, lessD_in_g(X1))
PB_IN_GA(X1, X2) → LESSD_IN_G(X1)
LESSD_IN_G(s(X1)) → U1_G(X1, lessD_in_g(X1))
LESSD_IN_G(s(X1)) → LESSD_IN_G(X1)
PB_IN_GA(X1, X2) → U3_GA(X1, X2, lesscD_in_g(X1))
U3_GA(X1, X2, lesscD_out_g(X1)) → U4_GA(X1, X2, insertA_in_gag(s(X1), X2, void))
U3_GA(X1, X2, lesscD_out_g(X1)) → INSERTA_IN_GAG(s(X1), X2, void)
INSERTA_IN_GAG(X1, tree(X1, void, X2), tree(X1, void, void)) → U10_GAG(X1, X2, pC_in_ga(X1, X2))
INSERTA_IN_GAG(X1, tree(X1, void, X2), tree(X1, void, void)) → PC_IN_GA(X1, X2)
PC_IN_GA(X1, X2) → U5_GA(X1, X2, lessD_in_g(X1))
PC_IN_GA(X1, X2) → LESSD_IN_G(X1)
PC_IN_GA(X1, X2) → U6_GA(X1, X2, lesscD_in_g(X1))
U6_GA(X1, X2, lesscD_out_g(X1)) → U7_GA(X1, X2, insertA_in_gag(X1, X2, void))
U6_GA(X1, X2, lesscD_out_g(X1)) → INSERTA_IN_GAG(X1, X2, void)
INSERTA_IN_GAG(s(X1), tree(s(X1), void, X2), tree(s(X1), void, void)) → U11_GAG(X1, X2, pB_in_ga(X1, X2))
INSERTA_IN_GAG(s(X1), tree(s(X1), void, X2), tree(s(X1), void, void)) → PB_IN_GA(X1, X2)
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U12_GAG(X1, X2, X3, X4, lessD_in_g(X1))
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → LESSD_IN_G(X1)
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U13_GAG(X1, X2, X3, X4, lesscD_in_g(X1))
U13_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → U14_GAG(X1, X2, X3, X4, insertA_in_gag(s(X1), X2, X4))
U13_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(s(X1), X2, X4)
INSERTA_IN_GAG(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U15_GAG(X1, X2, X3, X4, lessD_in_g(X1))
INSERTA_IN_GAG(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → LESSD_IN_G(X1)
INSERTA_IN_GAG(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U16_GAG(X1, X2, X3, X4, lesscD_in_g(X1))
U16_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → U17_GAG(X1, X2, X3, X4, insertA_in_gag(X1, X3, X4))
U16_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(X1, X3, X4)
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → U18_GAG(X1, X2, X3, X4, lessD_in_g(X1))
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → LESSD_IN_G(X1)
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → U19_GAG(X1, X2, X3, X4, lesscD_in_g(X1))
U19_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → U20_GAG(X1, X2, X3, X4, insertA_in_gag(s(X1), X3, X4))
U19_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(s(X1), X3, X4)
INSERTA_IN_GAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U21_GAG(X1, X2, X3, X4, insertA_in_gag(0, X2, X4))
INSERTA_IN_GAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → INSERTA_IN_GAG(0, X2, X4)
INSERTA_IN_GAG(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → U22_GAG(X1, X2, X3, X4, X5, lessF_in_gg(X1, X2))
INSERTA_IN_GAG(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → LESSF_IN_GG(X1, X2)
LESSF_IN_GG(s(X1), s(X2)) → U8_GG(X1, X2, lessF_in_gg(X1, X2))
LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U23_GAG(X1, X2, X3, X4, X5, lesscE_in_gg(X1, X2))
U23_GAG(X1, X2, X3, X4, X5, lesscE_out_gg(X1, X2)) → U24_GAG(X1, X2, X3, X4, X5, insertA_in_gag(s(X1), X3, X5))
U23_GAG(X1, X2, X3, X4, X5, lesscE_out_gg(X1, X2)) → INSERTA_IN_GAG(s(X1), X3, X5)
INSERTA_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U25_GAG(X1, X2, X3, X4, X5, lessF_in_gg(X2, X1))
INSERTA_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → LESSF_IN_GG(X2, X1)
INSERTA_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U26_GAG(X1, X2, X3, X4, X5, lesscF_in_gg(X2, X1))
U26_GAG(X1, X2, X3, X4, X5, lesscF_out_gg(X2, X1)) → U27_GAG(X1, X2, X3, X4, X5, insertA_in_gag(X1, X4, X5))
U26_GAG(X1, X2, X3, X4, X5, lesscF_out_gg(X2, X1)) → INSERTA_IN_GAG(X1, X4, X5)
INSERTA_IN_GAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U28_GAG(X1, X2, X3, X4, insertA_in_gag(s(X1), X3, X4))
INSERTA_IN_GAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTA_IN_GAG(s(X1), X3, X4)
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U29_GAG(X1, X2, X3, X4, X5, lessF_in_gg(X2, X1))
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSF_IN_GG(X2, X1)
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U30_GAG(X1, X2, X3, X4, X5, lesscF_in_gg(X2, X1))
U30_GAG(X1, X2, X3, X4, X5, lesscF_out_gg(X2, X1)) → U31_GAG(X1, X2, X3, X4, X5, insertA_in_gag(s(X1), X4, X5))
U30_GAG(X1, X2, X3, X4, X5, lesscF_out_gg(X2, X1)) → INSERTA_IN_GAG(s(X1), X4, X5)
lesscD_in_g(s(X1)) → U50_g(X1, lesscD_in_g(X1))
U50_g(X1, lesscD_out_g(X1)) → lesscD_out_g(s(X1))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(0), s(s(X1))) → lesscE_out_gg(s(0), s(s(X1)))
lesscE_in_gg(s(s(0)), s(s(s(X1)))) → lesscE_out_gg(s(s(0)), s(s(s(X1))))
lesscE_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscE_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscE_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscE_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscE_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U56_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U55_gg(X1, X2, lesscF_in_gg(X1, X2))
U55_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U56_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, void), tree(s(X1), void, void)) → U9_GAG(X1, X2, pB_in_ga(X1, X2))
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, void), tree(s(X1), void, void)) → PB_IN_GA(X1, X2)
PB_IN_GA(X1, X2) → U2_GA(X1, X2, lessD_in_g(X1))
PB_IN_GA(X1, X2) → LESSD_IN_G(X1)
LESSD_IN_G(s(X1)) → U1_G(X1, lessD_in_g(X1))
LESSD_IN_G(s(X1)) → LESSD_IN_G(X1)
PB_IN_GA(X1, X2) → U3_GA(X1, X2, lesscD_in_g(X1))
U3_GA(X1, X2, lesscD_out_g(X1)) → U4_GA(X1, X2, insertA_in_gag(s(X1), X2, void))
U3_GA(X1, X2, lesscD_out_g(X1)) → INSERTA_IN_GAG(s(X1), X2, void)
INSERTA_IN_GAG(X1, tree(X1, void, X2), tree(X1, void, void)) → U10_GAG(X1, X2, pC_in_ga(X1, X2))
INSERTA_IN_GAG(X1, tree(X1, void, X2), tree(X1, void, void)) → PC_IN_GA(X1, X2)
PC_IN_GA(X1, X2) → U5_GA(X1, X2, lessD_in_g(X1))
PC_IN_GA(X1, X2) → LESSD_IN_G(X1)
PC_IN_GA(X1, X2) → U6_GA(X1, X2, lesscD_in_g(X1))
U6_GA(X1, X2, lesscD_out_g(X1)) → U7_GA(X1, X2, insertA_in_gag(X1, X2, void))
U6_GA(X1, X2, lesscD_out_g(X1)) → INSERTA_IN_GAG(X1, X2, void)
INSERTA_IN_GAG(s(X1), tree(s(X1), void, X2), tree(s(X1), void, void)) → U11_GAG(X1, X2, pB_in_ga(X1, X2))
INSERTA_IN_GAG(s(X1), tree(s(X1), void, X2), tree(s(X1), void, void)) → PB_IN_GA(X1, X2)
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U12_GAG(X1, X2, X3, X4, lessD_in_g(X1))
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → LESSD_IN_G(X1)
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U13_GAG(X1, X2, X3, X4, lesscD_in_g(X1))
U13_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → U14_GAG(X1, X2, X3, X4, insertA_in_gag(s(X1), X2, X4))
U13_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(s(X1), X2, X4)
INSERTA_IN_GAG(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U15_GAG(X1, X2, X3, X4, lessD_in_g(X1))
INSERTA_IN_GAG(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → LESSD_IN_G(X1)
INSERTA_IN_GAG(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U16_GAG(X1, X2, X3, X4, lesscD_in_g(X1))
U16_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → U17_GAG(X1, X2, X3, X4, insertA_in_gag(X1, X3, X4))
U16_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(X1, X3, X4)
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → U18_GAG(X1, X2, X3, X4, lessD_in_g(X1))
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → LESSD_IN_G(X1)
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → U19_GAG(X1, X2, X3, X4, lesscD_in_g(X1))
U19_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → U20_GAG(X1, X2, X3, X4, insertA_in_gag(s(X1), X3, X4))
U19_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(s(X1), X3, X4)
INSERTA_IN_GAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U21_GAG(X1, X2, X3, X4, insertA_in_gag(0, X2, X4))
INSERTA_IN_GAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → INSERTA_IN_GAG(0, X2, X4)
INSERTA_IN_GAG(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → U22_GAG(X1, X2, X3, X4, X5, lessF_in_gg(X1, X2))
INSERTA_IN_GAG(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → LESSF_IN_GG(X1, X2)
LESSF_IN_GG(s(X1), s(X2)) → U8_GG(X1, X2, lessF_in_gg(X1, X2))
LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U23_GAG(X1, X2, X3, X4, X5, lesscE_in_gg(X1, X2))
U23_GAG(X1, X2, X3, X4, X5, lesscE_out_gg(X1, X2)) → U24_GAG(X1, X2, X3, X4, X5, insertA_in_gag(s(X1), X3, X5))
U23_GAG(X1, X2, X3, X4, X5, lesscE_out_gg(X1, X2)) → INSERTA_IN_GAG(s(X1), X3, X5)
INSERTA_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U25_GAG(X1, X2, X3, X4, X5, lessF_in_gg(X2, X1))
INSERTA_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → LESSF_IN_GG(X2, X1)
INSERTA_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U26_GAG(X1, X2, X3, X4, X5, lesscF_in_gg(X2, X1))
U26_GAG(X1, X2, X3, X4, X5, lesscF_out_gg(X2, X1)) → U27_GAG(X1, X2, X3, X4, X5, insertA_in_gag(X1, X4, X5))
U26_GAG(X1, X2, X3, X4, X5, lesscF_out_gg(X2, X1)) → INSERTA_IN_GAG(X1, X4, X5)
INSERTA_IN_GAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U28_GAG(X1, X2, X3, X4, insertA_in_gag(s(X1), X3, X4))
INSERTA_IN_GAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTA_IN_GAG(s(X1), X3, X4)
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U29_GAG(X1, X2, X3, X4, X5, lessF_in_gg(X2, X1))
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSF_IN_GG(X2, X1)
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U30_GAG(X1, X2, X3, X4, X5, lesscF_in_gg(X2, X1))
U30_GAG(X1, X2, X3, X4, X5, lesscF_out_gg(X2, X1)) → U31_GAG(X1, X2, X3, X4, X5, insertA_in_gag(s(X1), X4, X5))
U30_GAG(X1, X2, X3, X4, X5, lesscF_out_gg(X2, X1)) → INSERTA_IN_GAG(s(X1), X4, X5)
lesscD_in_g(s(X1)) → U50_g(X1, lesscD_in_g(X1))
U50_g(X1, lesscD_out_g(X1)) → lesscD_out_g(s(X1))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(0), s(s(X1))) → lesscE_out_gg(s(0), s(s(X1)))
lesscE_in_gg(s(s(0)), s(s(s(X1)))) → lesscE_out_gg(s(s(0)), s(s(s(X1))))
lesscE_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscE_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscE_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscE_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscE_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U56_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U55_gg(X1, X2, lesscF_in_gg(X1, X2))
U55_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U56_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
lesscD_in_g(s(X1)) → U50_g(X1, lesscD_in_g(X1))
U50_g(X1, lesscD_out_g(X1)) → lesscD_out_g(s(X1))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(0), s(s(X1))) → lesscE_out_gg(s(0), s(s(X1)))
lesscE_in_gg(s(s(0)), s(s(s(X1)))) → lesscE_out_gg(s(s(0)), s(s(s(X1))))
lesscE_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscE_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscE_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscE_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscE_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U56_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U55_gg(X1, X2, lesscF_in_gg(X1, X2))
U55_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U56_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
LESSF_IN_GG(s(X1), s(X2)) → LESSF_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
LESSD_IN_G(s(X1)) → LESSD_IN_G(X1)
lesscD_in_g(s(X1)) → U50_g(X1, lesscD_in_g(X1))
U50_g(X1, lesscD_out_g(X1)) → lesscD_out_g(s(X1))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(0), s(s(X1))) → lesscE_out_gg(s(0), s(s(X1)))
lesscE_in_gg(s(s(0)), s(s(s(X1)))) → lesscE_out_gg(s(s(0)), s(s(s(X1))))
lesscE_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscE_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscE_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscE_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscE_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U56_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U55_gg(X1, X2, lesscF_in_gg(X1, X2))
U55_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U56_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
LESSD_IN_G(s(X1)) → LESSD_IN_G(X1)
LESSD_IN_G(s(X1)) → LESSD_IN_G(X1)
From the DPs we obtained the following set of size-change graphs:
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U13_GAG(X1, X2, X3, X4, lesscD_in_g(X1))
U13_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(s(X1), X2, X4)
INSERTA_IN_GAG(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U16_GAG(X1, X2, X3, X4, lesscD_in_g(X1))
U16_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(X1, X3, X4)
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → U19_GAG(X1, X2, X3, X4, lesscD_in_g(X1))
U19_GAG(X1, X2, X3, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(s(X1), X3, X4)
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U23_GAG(X1, X2, X3, X4, X5, lesscE_in_gg(X1, X2))
U23_GAG(X1, X2, X3, X4, X5, lesscE_out_gg(X1, X2)) → INSERTA_IN_GAG(s(X1), X3, X5)
INSERTA_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U26_GAG(X1, X2, X3, X4, X5, lesscF_in_gg(X2, X1))
U26_GAG(X1, X2, X3, X4, X5, lesscF_out_gg(X2, X1)) → INSERTA_IN_GAG(X1, X4, X5)
INSERTA_IN_GAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → INSERTA_IN_GAG(0, X2, X4)
INSERTA_IN_GAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTA_IN_GAG(s(X1), X3, X4)
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U30_GAG(X1, X2, X3, X4, X5, lesscF_in_gg(X2, X1))
U30_GAG(X1, X2, X3, X4, X5, lesscF_out_gg(X2, X1)) → INSERTA_IN_GAG(s(X1), X4, X5)
lesscD_in_g(s(X1)) → U50_g(X1, lesscD_in_g(X1))
U50_g(X1, lesscD_out_g(X1)) → lesscD_out_g(s(X1))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(0), s(s(X1))) → lesscE_out_gg(s(0), s(s(X1)))
lesscE_in_gg(s(s(0)), s(s(s(X1)))) → lesscE_out_gg(s(s(0)), s(s(s(X1))))
lesscE_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscE_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscE_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscE_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscE_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U56_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U55_gg(X1, X2, lesscF_in_gg(X1, X2))
U55_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U56_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
INSERTA_IN_GAG(s(X1), tree(s(X1), X4, X3)) → U13_GAG(X1, X3, X4, lesscD_in_g(X1))
U13_GAG(X1, X3, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(s(X1), X4)
INSERTA_IN_GAG(X1, tree(X1, X2, X4)) → U16_GAG(X1, X2, X4, lesscD_in_g(X1))
U16_GAG(X1, X2, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(X1, X4)
INSERTA_IN_GAG(s(X1), tree(s(X1), X2, X4)) → U19_GAG(X1, X2, X4, lesscD_in_g(X1))
U19_GAG(X1, X2, X4, lesscD_out_g(X1)) → INSERTA_IN_GAG(s(X1), X4)
INSERTA_IN_GAG(s(X1), tree(s(X2), X5, X4)) → U23_GAG(X1, X2, X4, X5, lesscE_in_gg(X1, X2))
U23_GAG(X1, X2, X4, X5, lesscE_out_gg(X1, X2)) → INSERTA_IN_GAG(s(X1), X5)
INSERTA_IN_GAG(X1, tree(X2, X3, X5)) → U26_GAG(X1, X2, X3, X5, lesscF_in_gg(X2, X1))
U26_GAG(X1, X2, X3, X5, lesscF_out_gg(X2, X1)) → INSERTA_IN_GAG(X1, X5)
INSERTA_IN_GAG(0, tree(s(X1), X4, X3)) → INSERTA_IN_GAG(0, X4)
INSERTA_IN_GAG(s(X1), tree(0, X2, X4)) → INSERTA_IN_GAG(s(X1), X4)
INSERTA_IN_GAG(s(X1), tree(s(X2), X3, X5)) → U30_GAG(X1, X2, X3, X5, lesscF_in_gg(X2, X1))
U30_GAG(X1, X2, X3, X5, lesscF_out_gg(X2, X1)) → INSERTA_IN_GAG(s(X1), X5)
lesscD_in_g(s(X1)) → U50_g(X1, lesscD_in_g(X1))
U50_g(X1, lesscD_out_g(X1)) → lesscD_out_g(s(X1))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(0), s(s(X1))) → lesscE_out_gg(s(0), s(s(X1)))
lesscE_in_gg(s(s(0)), s(s(s(X1)))) → lesscE_out_gg(s(s(0)), s(s(s(X1))))
lesscE_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscE_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscE_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscE_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscE_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U56_gg(X1, X2, lesscF_in_gg(X1, X2))
lesscF_in_gg(0, s(X1)) → lesscF_out_gg(0, s(X1))
lesscF_in_gg(s(X1), s(X2)) → U55_gg(X1, X2, lesscF_in_gg(X1, X2))
U55_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscF_out_gg(s(X1), s(X2))
U56_gg(X1, X2, lesscF_out_gg(X1, X2)) → lesscE_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
lesscD_in_g(x0)
U50_g(x0, x1)
lesscE_in_gg(x0, x1)
lesscF_in_gg(x0, x1)
U55_gg(x0, x1, x2)
U56_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs: